Nuprl Definition : rng_nat_op
13,42
postcript
pdf
n
r
e
==
n
e
latex
clarification:
n
r
e
==
n
r
+gp
e
latex
Up
rings
1
Wellformedness Lemmas
rng
nat
op
wf
Definitions
n
e
,
r
+gp
origin
r e == n e
r e == n r
+gp e r e == n e
r e == n r+gp e e+gp